((APPEND (NIL . (DECL (*) (OT& (GROUND GROUND) . GROUND) CONSTANT NIL INFIX 800) . NIL . ((* . (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . (1 . * . INFIX . 800 .) . 1 . * .))) . NIL . NIL . NIL . NIL . NIL . APPEND . NIL . NIL . 1 .) ((((∀ U V)) (= (* U V) (CONDI (NULL U) V (CONS (CAR U) (* (CDR U) V))))) . (AXIOM (TM& ((∀ U V)) (= (* U V) (CONDI (NULL U) V (CONS (CAR U) (* (CDR U) V)))))) . NIL . ((CDR LISP . 7) (CAR LISP . 7) (CONS LISP . 6) (NULL LISP . 8) (V LISP . 1) (U LISP . 1) (* . 1)) . NIL . NIL . NIL . (2) . NIL . APPEND . NIL . NIL . 2 .) ((((∀ X U V)) (= (* (CONS X U) V) (CONS X (* U V)))) . (DECSIMP (TM& ((∀ X U V)) (= (* (CONS X U) V) (CONS X (* U V)))) SRIGHT (LR&) (LR&) (LR& (LISP . 12)) (LR& 2 (LISP . 14) (LISP . 15) (LISP . 16))) . NIL . ((* . 1) (V LISP . 1) (U LISP . 1) (X LISP . 2) (CONS LISP . 6)) . NIL . NIL . NIL . ((LISP . 16) (LISP . 15) (LISP . 14) 2 (LISP . 12)) . NIL . APPEND . NIL . NIL . 3 .) ((⊃ (∧ (LIST (* NNIL V)) (((∀ X U)) (⊃ (LIST (* U V)) (LIST (* (CONS X U) V))))) (((∀ U)) (LIST (* U V)))) . (∀E PHI (TM& ((λ U)) (LIST (* U V))) (LN& LISP . 17) (LR& (LISP . 12))) . NIL . ((V LISP . 1) (* . 1) (LIST LISP . 9) (CONS LISP . 6) (NNIL LISP . 5) (X LISP . 2) (U LISP . 1)) . NIL . NIL . NIL . ((LISP . 17) (LISP . 12)) . NIL . APPEND . NIL . NIL . 4 .) ((⊃ (((∀ X U)) (⊃ (LIST (* U V)) (LIST (CONS X (* U V))))) (((∀ U)) (LIST (* U V)))) . (REWRITE SRIGHT (LN& . 4) (LR& 3 2 (LISP . 13)) (LR& (LISP . 12))) . NIL . ((V LISP . 1) (* . 1) (LIST LISP . 9) (CONS LISP . 6) (X LISP . 2) (U LISP . 1)) . NIL . NIL . NIL . ((LISP . 17) (LISP . 16) (LISP . 15) (LISP . 14) 2 (LISP . 13) (LISP . 12)) . NIL . APPEND . NIL . NIL . 5 .) ((((∀ U V)) (LIST (* U V))) . (TAUT (TM& ((∀ U V)) (LIST (* U V))) (LR& 5 (LISP . 12))) . NIL . ((U LISP . 1) (LIST LISP . 9) (* . 1) (V LISP . 1)) . NIL . NIL . NIL . ((LISP . 12) (LISP . 13) 2 (LISP . 14) (LISP . 15) (LISP . 16) (LISP . 17)) . NIL . APPEND . NIL . NIL . 6 .) (NIL . (COMMENTL THE LAST TWO STEPS SHOULD BE DOABLE WITH A SINGLE DECSIMP BUT I HAVE NOT BEEN ABLE TO DO IT) . NIL . NIL . NIL . NIL . NIL . NIL . NIL . APPEND . NIL . NIL . 7 .)) (LISP (NIL . (DECL (U V W) (OT& . GROUND) VARIABLE LIST) . NIL . ((V . (VARIABLE . GROUND . LIST . NIL . NIL . 1 . V .)) (LIST . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (4 . LIST . PREFIX . 1000 .) . 1 . LIST .)) (U . (VARIABLE . GROUND . LIST . NIL . NIL . 1 . U .)) (W . (VARIABLE . GROUND . LIST . NIL . NIL . 1 . W .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 1 .) (NIL . (DECL (X Y Z) (OT& . GROUND) VARIABLE SEXP) . NIL . ((Y . (VARIABLE . GROUND . SEXP . NIL . NIL . 2 . Y .)) (SEXP . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (4 . SEXP . PREFIX . 1000 .) . 2 . SEXP .)) (X . (VARIABLE . GROUND . SEXP . NIL . NIL . 2 . X .)) (Z . (VARIABLE . GROUND . SEXP . NIL . NIL . 2 . Z .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 2 .) (NIL . (DECL (A B C) (OT& . GROUND) VARIABLE) . NIL . ((B . (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . 3 . B .)) (A . (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . 3 . A .)) (C . (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . 3 . C .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 3 .) (NIL . (DECL (PHI) (OT& (GROUND) . TRUTHVAL) VARIABLE) . NIL . ((PHI . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 4 . PHI .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 4 .) (NIL . (DECL (NNIL) (OT& . GROUND) CONSTANT LIST) . NIL . ((LIST . 1) (NNIL . (CONSTANT . GROUND . LIST . NIL . NIL . 5 . NNIL .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 5 .) (NIL . (DECL (CONS) (OT& (GROUND GROUND) . GROUND) CONSTANT) . NIL . ((CONS . (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 6 . CONS .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 6 .) (NIL . (DECL (CAR CDR) (OT& (GROUND) . GROUND) CONSTANT) . NIL . ((CAR . (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 7 . CAR .)) (CDR . (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 7 . CDR .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 7 .) (NIL . (DECL (NULL) (OT& (GROUND) . TRUTHVAL) CONSTANT) . NIL . ((NULL . (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 8 . NULL .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 8 .) (NIL . (DECL (LIST) (OT& (GROUND) . TRUTHVAL) CONSTANT) . NIL . ((LIST . (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 9 . LIST .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 9 .) (NIL . (DECL (SEXP) (OT& (GROUND) . TRUTHVAL) CONSTANT) . NIL . ((SEXP . (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 10 . SEXP .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 10 .) ((((∀ U)) (SEXP U)) . (AXIOM (TM& ((∀ U)) (SEXP U))) . NIL . ((SEXP . 10) (U . 1)) . NIL . NIL . NIL . (11) . NIL . LISP . NIL . NIL . 11 .) ((((∀ X U)) (LIST (CONS X U))) . (AXIOM (TM& ((∀ X U)) (LIST (CONS X U)))) . NIL . ((LIST . 9) (CONS . 6) (X . 2) (U . 1)) . NIL . NIL . NIL . (12) . NIL . LISP . NIL . NIL . 12 .) ((((∀ U)) (≡ (NULL U) (= U NNIL))) . (AXIOM (TM& ((∀ U)) (≡ (NULL U) (= U NNIL)))) . NIL . ((NULL . 8) (NNIL . 5) (U . 1)) . NIL . NIL . NIL . (13) . NIL . LISP . NIL . NIL . 13 .) ((((∀ X U)) (¬ (NULL (CONS X U)))) . (AXIOM (TM& ((∀ X U)) (¬ (NULL (CONS X U))))) . NIL . ((NULL . 8) (CONS . 6) (X . 2) (U . 1)) . NIL . NIL . NIL . (14) . NIL . LISP . NIL . NIL . 14 .) ((((∀ X U)) (= (CAR (CONS X U)) X)) . (AXIOM (TM& ((∀ X U)) (= (CAR (CONS X U)) X))) . NIL . ((CAR . 7) (CONS . 6) (X . 2) (U . 1)) . NIL . NIL . NIL . (15) . NIL . LISP . NIL . NIL . 15 .) ((((∀ X U)) (= (CDR (CONS X U)) U)) . (AXIOM (TM& ((∀ X U)) (= (CDR (CONS X U)) U))) . NIL . ((CDR . 7) (CONS . 6) (X . 2) (U . 1)) . NIL . NIL . NIL . (16) . NIL . LISP . NIL . NIL . 16 .) ((((∀ PHI)) (⊃ (∧ (PHI NNIL) (((∀ X U)) (⊃ (PHI U) (PHI (CONS X U))))) (((∀ U)) (PHI U)))) . (AXIOM (TM& ((∀ PHI)) (⊃ (∧ (PHI NNIL) (((∀ X U)) (⊃ (PHI U) (PHI (CONS X U))))) (((∀ U)) (PHI U))))) . NIL . ((CONS . 6) (NNIL . 5) (PHI . 4) (X . 2) (U . 1)) . NIL . NIL . NIL . (17) . NIL . LISP . NIL . NIL . 17 .)) (COPY (NIL . (DECL (COPY) (OT& (GROUND) . GROUND) CONSTANT) . NIL . ((COPY . (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 1 . COPY .))) . NIL . NIL . NIL . NIL . NIL . COPY . NIL . NIL . 1 .) ((((∀ U)) (= (COPY U) (CONDI (NULL U) NNIL (CONS (CAR U) (COPY (CDR U)))))) . (AXIOM (TM& ((∀ U)) (= (COPY U) (CONDI (NULL U) NNIL (CONS (CAR U) (COPY (CDR U))))))) . NIL . ((U LISP . 1) (NNIL LISP . 5) (CONS LISP . 6) (CAR LISP . 7) (CDR LISP . 7) (NULL LISP . 8) (COPY . 1)) . NIL . NIL . NIL . (2) . NIL . COPY . NIL . NIL . 2 .) ((⊃ (∧ (= (COPY NNIL) NNIL) (((∀ X U)) (⊃ (= (COPY U) U) (= (COPY (CONS X U)) (CONS X U))))) (((∀ U)) (= (COPY U) U))) . (∀E PHI (TM& ((λ V)) (= (COPY V) V)) (LN& LISP . 17) (LR& (LISP . 12))) . NIL . ((U LISP . 1) (X LISP . 2) (NNIL LISP . 5) (CONS LISP . 6) (COPY . 1)) . NIL . NIL . NIL . ((LISP . 17) (LISP . 12)) . NIL . COPY . NIL . NIL . 3 .) ((((∀ X U)) (= (COPY (CONS X U)) (CONS X (COPY U)))) . (DECSIMP (TM& ((∀ X U)) (= (COPY (CONS X U)) (CONS X (COPY U)))) SRIGHT (LR&) (LR&) (LR& (LISP . 12)) (LR& 2 (LISP . 14) (LISP . 15) (LISP . 16))) . NIL . ((COPY . 1) (U LISP . 1) (X LISP . 2) (CONS LISP . 6)) . NIL . NIL . NIL . ((LISP . 16) (LISP . 15) (LISP . 14) 2 (LISP . 12)) . NIL . COPY . NIL . NIL . 4 .) ((((∀ U)) (= (COPY U) U)) . (DECSIMP (TM& ((∀ U)) (= (COPY U) U)) SRIGHT (LR& 3) (LR&) (LR& (LISP . 12)) (LR& 2 (LISP . 13) 4)) . NIL . ((COPY . 1) (U LISP . 1)) . NIL . NIL . NIL . ((LISP . 12) 2 (LISP . 14) (LISP . 15) (LISP . 16) (LISP . 13) (LISP . 17)) . NIL . COPY . NIL . NIL . 5 .)) (LIST ((((∀ U V)) (= (* U V) (CONDI (NULL U) V (CONS (CAR U) (* (CDR U) V))))) . (AXIOM (TM& ((∀ U V)) (= (* U V) (CONDI (NULL U) V (CONS (CAR U) (* (CDR U) V)))))) . NIL . ((* APPEND . 1) (U . (VARIABLE . (VAR& . VTYP1) . UNIVERSAL . NIL . NIL . 1 . U .)) (V . (VARIABLE . (VAR& . VTYP2) . UNIVERSAL . NIL . NIL . 1 . V .)) (NULL . (VARIABLE . (VAR& . VTYP3) . UNIVERSAL . NIL . NIL . 1 . NULL .)) (CONS . (VARIABLE . (VAR& . VTYP4) . UNIVERSAL . NIL . NIL . 1 . CONS .)) (CAR . (VARIABLE . (VAR& . VTYP5) . UNIVERSAL . NIL . NIL . 1 . CAR .)) (CDR . (VARIABLE . (VAR& . VTYP6) . UNIVERSAL . NIL . NIL . 1 . CDR .))) . NIL . ((VTYP6 (GROUND) . GROUND) (VTYP3 (GROUND) . TRUTHVAL) (VTYP2 . GROUND) (VTYP1 . GROUND) (VTYP5 (GROUND) VAR& . VTYP8) (VTYP4 ((VAR& . VTYP8) GROUND) VAR& . VTYP10)) . NIL . (1) . NIL . LIST . NIL . NIL . 1 .)))